﻿/************************************************************************
 * SMLib - State Model Library
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     SMLib\Automata\DFA\DFA_EquivChecker.cs
 * Description  :     Check equivalency of two DFAs
 * Change log   :     -Dec 2012: Initial Version
 * To Do        :     
 ************************************************************************/
using System;
using System.Collections.Generic;
using SMLib.Automata.Base;
using SMLib.Utils;

namespace SMLib.Automata.DFA
{
    /// <summary>
    /// Check equivalency of two DFAs
    /// </summary>
    public class DFA_EquivChecker
    {
        /// <summary>
        /// Two corresponding nodes (of two DFAs), AND the word we have seen to this state.
        /// It is used in Hopcroft-Karp Algorithm (function EquivalenceQuery, bellow) to compare two DFAs.
        /// </summary>
        struct CorrespondingNodes
        {
            public CorrespondingNodes(DFA.DFA_State k, DFA.DFA_State v)
            {
                Key = k;
                Value = v;
                path = new Word();
            }

            public CorrespondingNodes(DFA.DFA_State k, DFA.DFA_State v, Word prevPath, ISymbol step)
            {
                Key = k;
                Value = v;
                path = new Word(prevPath);
                path.AddSymbol(step);
            }

            public DFA.DFA_State Key;
            public DFA.DFA_State Value;
            public Word path;
        }

        /// <summary>
        /// See whether two DFA are equal or not. If they are not equal, find a counterexample to show the difference
        /// Based on Hopcroft-Karp Algorithm [A linear algorithm for testing equivalence of finite automata]
        /// </summary>
        /// <param name="SUT">first DFA (usualy the original SUT)</param>
        /// <param name="conjucture">second DFA (usualy the conjecture learnt by a learner)</param>
        /// <returns>
        /// if null, the models are the same.
        /// if not, it is a counterexample which shows the models are not the same
        /// </returns>
        public Word FindCounterexample(DFA SUT, DFA conjucture)
        {
            Stack<CorrespondingNodes> st = new Stack<CorrespondingNodes>();
            List<FlaggedList<DFA.DFA_State>> allSets = new List<FlaggedList<DFA.DFA_State>>();

            //For every state q in Q1 union Q2 , MakeSet(q)
            foreach (DFA.DFA_State n in SUT.GetStates())
            {
                FlaggedList<DFA.DFA_State> equivalents = new FlaggedList<DFA.DFA_State>();
                equivalents.Add(n);
                equivalents.flag = n.isAccepting;
                allSets.Add(equivalents);
            }
            foreach (DFA.DFA_State n in conjucture.GetStates())
            {
                FlaggedList<DFA.DFA_State> equivalents = new FlaggedList<DFA.DFA_State>();
                equivalents.Add(n);
                equivalents.flag = n.isAccepting;
                allSets.Add(equivalents);
            }

            //Union(s1,s2) 
            FlaggedList<DFA.DFA_State> s1, s2;
            s1 = allSets[0];
            s2 = allSets[SUT.Size];
            s1.Union(s2);
            allSets.RemoveAt(SUT.Size);

            //Push (s1,s2) on the stack
            st.Push(new CorrespondingNodes((DFA.DFA_State)SUT[0], (DFA.DFA_State)conjucture[0]));

            //While S is non-empty
            while (st.Count != 0)
            {
                //Pop pair (q1; q2) from S
                CorrespondingNodes c = st.Pop();
                Word curentWord = c.path;

                //For each a in Sigma 
                foreach (ISymbol a in SUT.InputAlphabet.AllSymbols())
                {

                    DFA.DFA_State nextA = c.Key.NextState(a);
                    DFA.DFA_State nextB = c.Value.NextState(a);
                    int setOfA = -1, setOfB = -1;
                    for (int i = 0; i < allSets.Count; i++)
                    {
                        if (allSets[i].Contains(nextA))
                            setOfA = i;

                        if (allSets[i].Contains(nextB))
                            setOfB = i;

                        if (setOfA > -1 && setOfB > -1) break;
                    }
                    //if r1<>r2
                    if (setOfA != setOfB)
                    {
                        if (allSets[setOfA].flag == allSets[setOfB].flag)
                            allSets[setOfA].Union(allSets[setOfB]);
                        else
                        {
                            Word counterExample = new Word(curentWord);
                            counterExample.AddSymbol(a);
                            return counterExample;
                        }
                        allSets.RemoveAt(setOfB);
                        CorrespondingNodes ns = new CorrespondingNodes(nextA, nextB);
                        ns.path = new Word(curentWord);
                        ns.path.AddSymbol(a);
                        st.Push(ns);
                    }
                }
            }
            return null;
        }
    }
}
